Nuprl Lemma : qadd_preserves_qless
11,40
postcript
pdf
a
,
b
,
c
:
. {
a
<
b
c
+
a
<
c
+
b
}
latex
Definitions
T
,
,
True
,
t
T
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
{
T
}
,
x
:
A
.
B
(
x
)
,
S
T
Lemmas
mon
ident
q
,
qinverse
q
,
qadd
comm
q
,
qadd
ac
1
q
,
true
wf
,
squash
wf
,
int
inc
rationals
,
qmul
wf
,
grp
op
preserves
lt
qorder
,
rationals
wf
,
qadd
wf
,
qless
wf
origin
a, b, c:
. {a < b 
c + a < c + b} a, b, c:. {a < b c + a < c + b} 
T
T Q Q Qx:A. B(x)
T